\begin{tabbing}
$\forall$$M_{1}$, $M_{2}$:MsgA.
\\[0ex]$M_{1}$ $\subseteq$ $M_{2}$
\\[0ex]$\Rightarrow$ (\=$\forall$\=$k$:Knd, $l$:IdLnk, $s$:$M_{2}$.state, $v$:$M_{2}$.da($k$), $i$:Id,\+\+
\\[0ex]${\it ms}$:(${\it tg}$:Id$\times$if source($l$) = $i$$\rightarrow$ $M_{2}$.da(rcv($l$,${\it tg}$)) else Top fi) List.
\-\\[0ex]$M_{2}$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$) $\Rightarrow$ $M_{1}$.send($k$;$l$;$s$;$v$;${\it ms}$;$i$))
\-
\end{tabbing}